/*
 * Atomic Predicates for Transformers
 * 
 * Copyright (c) 2015 UNIVERSITY OF TEXAS AUSTIN. All rights reserved. Developed
 * by: HONGKUN YANG and SIMON S. LAM http://www.cs.utexas.edu/users/lam/NRL/
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * with the Software without restriction, including without limitation the
 * rights to use, copy, modify, merge, publish, distribute, sublicense, and/or
 * sell copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * 1. Redistributions of source code must retain the above copyright notice,
 * this list of conditions and the following disclaimers.
 * 
 * 2. Redistributions in binary form must reproduce the above copyright notice,
 * this list of conditions and the following disclaimers in the documentation
 * and/or other materials provided with the distribution.
 * 
 * 3. Neither the name of the UNIVERSITY OF TEXAS AUSTIN nor the names of the
 * developers may be used to endorse or promote products derived from this
 * Software without specific prior written permission.
 * 
 * 4. Any report or paper describing results derived from using any part of this
 * Software must cite the following publication of the developers: Hongkun Yang
 * and Simon S. Lam, Scalable Verification of Networks With Packet Transformers
 * Using Atomic Predicates, IEEE/ACM Transactions on Networking, October 2017,
 * Volume 25, No. 5, pages 2900-2915 (first published as IEEE Early Access
 * Article, July 2017, Digital Object Identifier: 10.1109/TNET.2017.2720172).
 * 
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * CONTRIBUTORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS WITH
 * THE SOFTWARE.
 */
package transformer;

import java.io.IOException;
import java.util.*;
import java.util.Map.Entry;

import common.BDDACLWrapper;
import common.Fields;
import common.PositionTuple;

public class StateTransfer extends AbstractStateTransfer{


    public StateTransfer(Net net) {
        super(net);
    }

    /**
     * return the head state
     */
    public StateBDD Traverse(PositionTuple startpt, PositionTuple endpt)
    {
        reset_reachsets();

        destination = endpt;
        Device d = (Device) net.getBox(startpt.getDeviceName());
        int inject_pkt = BDDACLWrapper.BDDFalse;
        if(d.fwbdds.containsKey(startpt.getPortName()))
        {
            inject_pkt = d.fwbdds.get(startpt.getPortName());
            net.bddengine.ref(inject_pkt);
        }
        StateBDD startstate = new StateBDD(startpt, inject_pkt);
        Traverse_recur(startstate);
        return startstate;
    }

    /**
     * return the head state
     */
    public StateBDD Traverse(PositionTuple startpt)
    {
        reset_reachsets();

        
        destination = null;
        Device d = (Device) net.getBox(startpt.getDeviceName());
        int inject_pkt = BDDACLWrapper.BDDFalse;
        if(d.fwbdds.containsKey(startpt.getPortName()))
        {
            inject_pkt = d.fwbdds.get(startpt.getPortName());
            net.bddengine.ref(inject_pkt);
        }
        StateBDD startstate = new StateBDD(startpt, inject_pkt);
        Traverse_recur(startstate);
        return startstate;
    }

    /**
     * return the head state
     */
    public StateBDD TraverseAnyPkt(PositionTuple startpt)
    {
        reset_reachsets();

        
        destination = null;
        StateBDD startstate = new StateBDD(startpt, BDDACLWrapper.BDDTrue);
        Traverse_recur(startstate);
        return startstate;
    }

    public StateBDD TraverseAnyNonTunnelPkt(PositionTuple startpt)
    {
        reset_reachsets();
        
        destination  = null;
        int injected_pkt = net.bddengine.set_field_bit(Fields.dst_ip_inner, BDDACLWrapper.BDDTrue, false);
        //System.out.println("injected:" + injected_pkt);
        StateBDD startstate = new StateBDD(startpt, injected_pkt);
        Traverse_recur(startstate);
        return startstate;
    }

    public StateBDD TraverseAnyNonMPLSPkt(PositionTuple startpt)
    {
        reset_reachsets();
        
        destination  = null;
        int injected_pkt = net.bddengine.set_field_bit(Fields.mpls_label, BDDACLWrapper.BDDTrue, false);
        StateBDD startstate = new StateBDD(startpt, injected_pkt);
        Traverse_recur(startstate);
        return startstate;
    }

    public StateBDD TraverseCombPkt(PositionTuple startpt)
    {
        reset_reachsets();
        
        destination = null;
        // all non mpls pkt
        int no_mpls_pkt = net.bddengine.mplsLabelField;
        // select from forwarding table
        int prefix = net.bddengine.encodeDstIPPrefix(136200192, 24);
        int inject_pkt = net.bddengine.ref(net.bddengine.or(no_mpls_pkt, prefix));
        StateBDD startstate = new StateBDD(startpt, inject_pkt);
        Traverse_recur(startstate);
        return startstate;
    }

    /**
     * this is the original implementation of traverse_recur 
     * 
      public void Traverse_recur(State s)
      {
            PositionTuple curpt = s.getPosition();
            HashSet<PositionTuple> nxtpts = net.LinkTransfer(curpt);
            State nxts = null;
            if(nxtpts == null)
            {
                  return;
            }else{

                  for(PositionTuple nxtpt : nxtpts)
                  {

                        int faps = s.getAPSet();
                        nxts = new State(nxtpt,faps, s.getAlreadyVisited(), s.getPtAlreadyVisited());
                        s.addNextState(nxts);


                        //if(nxts.loopDetected())
                        if(nxts.ptLoopDetected())
                        {
                              continue;
                        }
                        if(destination != null)
                        {
                              if(nxts.destDetected(destination))
                              {
                                    continue;
                              }
                        }

                        // next one is the switch forwarding
                        Box nxtd = net.getBox(nxtpt.getDeviceName());
                        if(nxtd == null)
                        {
                              continue;
                        }
                        int fwdaps = nxts.getAPSet();
                        HashMap<String, Integer> fwdset =  nxtd.ForwardAction(nxtpt.getPortName(), fwdaps);
                        if(fwdset.isEmpty())
                        {
                              continue;
                        }else
                        {
                              Iterator iter = fwdset.entrySet().iterator();
                              //for(String portname : fwdset.keySet())
                              while(iter.hasNext())
                              {
                                    Map.Entry<String, Integer> oneentry = (Entry<String, Integer>) iter.next();
                                    PositionTuple fwdedpt = new PositionTuple(nxtpt.getDeviceName(), oneentry.getKey());
                                    //State fwdeds = new State(fwdedpt, fwdset.get(portname), nxts.getAlreadyVisited());
                                    State fwdeds = new State(fwdedpt, oneentry.getValue(), nxts.getAlreadyVisited(), 
                                                nxts.getPtAlreadyVisited());
                                    nxts.addNextState(fwdeds);
                                    //if(!fwdeds.loopDetected() && !fwdeds.destDetected(destination))
                                    Traverse_recur(fwdeds);
                              }
                        }
                  }

            }
      }
     **/
    public static void main (String[] args) throws IOException
    {
        Network n = new Network("i2");
        StateTransfer stfer = new StateTransfer(n);
        long start = System.nanoTime();
        StateBDD hs = null;
        //for(int i = 0; i < 10000; i ++)
        {
            //hs = stfer.Traverse(new PositionTuple("kans","xe-0/1/1"), new PositionTuple("salt","ge-6/0/0"));
            hs = stfer.TraverseAnyPkt(new PositionTuple("kans","xe-0/1/1"));
        }
        long end = System.nanoTime();
        hs.printState();
        System.out.println(hs.tree_size()+" nodes");
        System.out.println((end - start)/1000000.0);
    }

    @Override
    public AbstractState getNxtStateLink(AbstractState s, PositionTuple pt) {

        int faps = ((StateBDD)s).getAPSet();
        StateBDD nxts = new StateBDD(pt, faps, s.getAlreadyVisited(), s.getPtAlreadyVisited());
        return nxts;
    }

    @Override
    public AbstractState getNxtStateFwd(Object iter_obj, AbstractState s) {
        Map.Entry<String, Integer> oneentry = (Entry<String, Integer>) iter_obj;
        PositionTuple fwdedpt = new PositionTuple(s.getPosition().getDeviceName(), oneentry.getKey());
        StateBDD fwdeds = new StateBDD(fwdedpt, oneentry.getValue(), s.getAlreadyVisited(), 
                s.getPtAlreadyVisited());

        return fwdeds;
    }

    @Override
    public Iterator getForwardingEntries(AbstractState s) {
        Box nxtd = net.getBox(s.getPosition().getDeviceName());
        if(nxtd == null)
        {
            return null;
        }
        int fwdaps = ((StateBDD) s).getAPSet();
        HashMap<String, Integer> fwdset =  nxtd.ForwardAction(s.getPosition().getPortName(), fwdaps);
        return fwdset.entrySet().iterator();
    }

}
